/*
 * To change this template, choose Tools | Templates
 * and open the template in the editor.
 */

/**
 * NuGat-API named Chameleon developed by Simon De Baets to Verimag.
 *
 */


package chameleon.model.NuGatManager.Strategy;

import chameleon.model.NuGatStructure.game.GamePlayer;
import chameleon.model.NuGatStructure.prop.PropGame;
import chameleon.model.NuGatStructure.prop.Prop;
import chameleon.model.NuGatStructure.opt.OptGame;
import chameleon.model.NuGatStructure.utils.Node;
import chameleon.model.NuGatStructure.fsm.GameBddFsm;
import chameleon.model.NuGatStructure.bdd.Bdd;
import chameleon.model.NuGatStructure.bdd.DdManager;
import chameleon.model.NuGatStructure.enc.BddEnc;
import chameleon.gameSolver.NuGat.NuGatInterface;
import chameleon.view.OutputManager;
import com.sun.jna.Pointer;
import java.io.IOException;

/**
 * This class computes the preimage for a given target which use the NuGat/NuSmv
 * methods.
 * @author simon
 */
public class PreImageComputation {
    
    private NuGatInterface nugat_;
    private PropGame prop_;


    public PreImageComputation (NuGatInterface nugat, PropGame prop){
        nugat_ = nugat;
        checkProperty(prop);
        prop_ = prop;
    }
    
    private void checkProperty(Prop prop){
        assert (nugat_.PropGame_ReachTarget == prop.getType()
                || nugat_.PropGame_ReachDeadlock == prop.getType()
                || nugat_.PropGame_AvoidTarget == prop.getType()
                || nugat_.PropGame_AvoidDeadlock == prop.getType());
    }


     /**
         * This code is an adaptation of the NuGat code provide in file
         * gameCheckReachAvoidSpec.c, in function Game_UseStrongReachabilityAlgorithm.
         */

    public PreImage compute(BddEnc enc, OptGame oh, GameBddFsm gameBddFsm){
        

        //initialisation of the system

        nugat_.Game_BeforeCheckingSpec(prop_.ptr());

        DdManager ddManager = enc.getDdManager();

        /* flag which player this game is for */

        GamePlayer PLAYER_1 = new GamePlayer(nugat_.PLAYER_NAME_1,nugat_);
        GamePlayer PLAYER_2 = new GamePlayer(nugat_.PLAYER_NAME_2,nugat_);

        String left = nugat_.get_text(nugat_.find_string(nugat_.PLAYER_NAME_1));
        String right = prop_.getPlayer();
        
        GamePlayer player =
            (left.equals(right))
            ? PLAYER_1 : PLAYER_2;
        
        GamePlayer opponent = PLAYER_1.equals(player) ? PLAYER_2 : PLAYER_1;
        char quantifiers = oh.gameInitialCondition();

        Bdd init_1, init_2, invar_1, invar_2;
        Bdd originalTarget;  /* A target to be reached. */
        Bdd allReachStates;  /* All the states from which the target can
                                  be reached. */
        Node reachStateList = new Node (Pointer.NULL,nugat_);
                            /* A list of consecutive states from which
                                  the target can be reached. */
        boolean isTargetReached; /* True if the target is reachable by a
                                  player (for reachability game) or an
                                  opponent (for avoidance game). */
        boolean isFixedpointReached = false;
        int pathLength = 0;


        /* prepare the initial states (obtain them and add the invariants) */
        init_1 = gameBddFsm.getInit1();
        init_2 = gameBddFsm.getInit2();
        invar_1 = gameBddFsm.getInvars1();
        invar_2 = gameBddFsm.getInvars2();



        //originally bddAndAccumulate

        init_1 = ddManager.bddAndAccumulate( init_1, invar_1);
        init_2 = ddManager.bddAndAccumulate( init_2, invar_2);

        /* initialize the original target states (reachability or avoidance target) */
        if (nugat_.PropGame_ReachTarget == prop_.getType() ||
            nugat_.PropGame_AvoidTarget == prop_.getType()) {
            originalTarget =
                enc.exprToBdd(prop_.getExprCore(),
                    new Node (Pointer.NULL,nugat_));
        }
        else {
            /* create empty set of target states */
            originalTarget = ddManager.bddZero();
        }

        
        //originally bddAndAccumulate
        originalTarget = ddManager.bddAndAccumulate(originalTarget, invar_1);
        originalTarget = ddManager.bddAndAccumulate(originalTarget, invar_2);

        /* For avoidance games it is necessary to reverse the player and, as
            result, initial quantifiers (because now we play for the
            opponent).
         */

        if (nugat_.PropGame_AvoidTarget == prop_.getType() ||
            nugat_.PropGame_AvoidDeadlock == prop_.getType()) {
                player = PLAYER_1.equals(player) ? PLAYER_2 : PLAYER_1;
                opponent = PLAYER_1.equals(opponent) ? PLAYER_2 : PLAYER_1;

                if (quantifiers == 'N')
                    quantifiers = 'N';
                else if (quantifiers == 'E')
                    quantifiers = 'A';
                else if (quantifiers == 'A')
                    quantifiers = 'E';
                else
                    new IOException("unknown quantifiers");
         }
        
        allReachStates = ddManager.bddDup(originalTarget);
        reachStateList = reachStateList.cons(
                new Node(ddManager.bddDup(originalTarget).ptr(),nugat_),
                new Node (Pointer.NULL, nugat_));

        /*int isTargetReachd= nugat_.isTargetReached(fsm,init_1.ptr(), init_2.ptr(),
                allReachStates.ptr(),player,quantifiers);
        
        isTargetReached = (isTargetReachd == 1);*/
        
        isTargetReached = gameBddFsm.canPlayerSatisfy(init_1,
                init_2,
                allReachStates,
                player,
                quantifiers);
        
        /* Makes a few checks and prints a few warning in the case of
             suspicious input, i.e., if init is zero, target is zero or one.
          */
          {
              OutputManager output = new OutputManager();
            /* init is zero */
            if (ddManager.bddIsZero(init_1) || ddManager.bddIsZero(init_2)) {
                String playerMess = ddManager.bddIsZero(init_1) ? "player 1 ": "player 2";
              output.displayString(""+
                        "\n********   WARNING   ********\n"+
                      "Initial states set for "+playerMess+" is empty.\n"+
                      "******** END WARNING ********\n");
                      
              /* to skip the loop below */
              isFixedpointReached = true;
            }
            /* target is zero (check only reach-target and avoid-target specs) */
            if ((nugat_.PropGame_ReachTarget == prop_.getType()
                 || nugat_.PropGame_AvoidTarget == prop_.getType())
                && ddManager.bddIsZero(originalTarget)) {
              output.displayString(""+
                        "\n********   WARNING   ********\n"+
                      "The target states set is empty.\n"+
                      "******** END WARNING ********\n");
              /* continue the check because deadlock state may allow to win */
            }
            /* target is reached at step zero */
            if (isTargetReached) {
              output.displayString(""+
                        "\n********   WARNING   ********\n"+
                      "The target states are reached at step 0.\n"+
                      "Probably this is not what was intended.\n"+
                      "******** END WARNING ********\n");
            }
          }


          
         /* ------------ main loop ------------------*/
        /* loops stop if fixed-point is reached or target is reached from init */

         while (!isFixedpointReached && !isTargetReached) {

            Bdd previousReachStates = ddManager.bddDup(allReachStates);

            Bdd preImage = computeOneStep(gameBddFsm,allReachStates,player);
            
            allReachStates = ddManager.bddOrAccumulate(allReachStates, preImage);

            isFixedpointReached = previousReachStates.equals(allReachStates);
            

            /* check reachability only if fixpoint has not been reached */
            if (!isFixedpointReached) {
              isTargetReached = gameBddFsm.canPlayerSatisfy(init_1,
                init_2,
                allReachStates,
                player,
                quantifiers);
            }
            
            
            /* add to the list of reach states sets */
            reachStateList = reachStateList.cons(new Node(
                    (ddManager.bddDup(allReachStates)).ptr(),nugat_),
                    new Node (reachStateList.ptr(),nugat_));
            
            pathLength++;
            
            
            ddManager.bddFree(previousReachStates);
            ddManager.bddFree(preImage);
            
        }
         
         
        ddManager.bddFree(init_1);
        ddManager.bddFree(init_2);
        ddManager.bddFree(invar_1);
        ddManager.bddFree(invar_2);
        
        return new PreImage(prop_, reachStateList, nugat_,isTargetReached,
                isFixedpointReached,player,opponent,
                quantifiers, originalTarget, allReachStates);

    }
    

    /**
     * This function compute the next Pre-Image.
     *
     *
     * @param fsm (GameBddFsmDecorator)
     * @param target (bdd_ptr)
     * @param player (GamePlayer)
     * @return preImage (bdd_ptr)
     */

    private Bdd computeOneStep(GameBddFsm fsm, Bdd target,
            GamePlayer player){

            Bdd preImage;


            // pre-image can be computed with not-reach-state constraint on
            // returned value, since only "new" reach states are of importance.
            // This can speed up computation of pre-image.

            /* compute the strong pre-image for reach states and given player. */
            preImage =  fsm.getStrongBackwardImage(target, player);

            return preImage;
    }


}
